RCS "$Id: HMLCheck.sig,v 1.6 1998/08/13 11:38:48 pxs Exp $";
(********************************** HMLSat ***********************************)
(*                                                                           *)
(* This file contains the signature for model checking on predefined graphs. *)
(*                                                                           *)
(*****************************************************************************)

signature HMLCHECK =
sig
   structure PG : POLYGRAPH

   eqtype mcinfo
   type prop

   val setmcinfo : PG.Ag.agent -> mcinfo
   val check : (mcinfo PG.state ref * mcinfo PG.state ref list) -> prop -> bool
end


